$\forall$${\it MA}$:MsgA, $s$:${\it MA}$.state, $k$:Knd, $l$:IdLnk, ${\it vaal}$:${\it MA}$.V($k$).
\\[0ex]($\neg$($\uparrow<$$k$, $l$$>$ $\in$ dom((${\it MA}$.2.2.2.2.2).1)))
\\[0ex]$\Rightarrow$ (filter($\lambda$${\it ms}$.eqof(IdLnkDeq)(mlnk(${\it ms}$),$l$);${\it MA}$.sends($k$,$s$,${\it vaal}$)) $\sim$ [])